((v1 v3 8) (v6 v4 1) (v6 v3 1) (v5 v1 9) (v4 v2 0) (v4 v1 1) (v3 v5 4) (v5 v6 2) (v6 v2 1) (v2 v1 5)) 57 ((v3 v4) (v6 v3) (v4 v2))